es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E. f2f+-pred(e',e)   

latex

Definitions	A c B, t.2, t.1, P  Q, is_ack , x:A. B(x), is_req  , [e: i p j], P & Q, P  Q, f2f+-pred(e',e), , t  T, F2F+-decls, FIFO, x:A. B(x), [e: i p j]
Lemmas	event system wf, fifo wf, es-state wf, top wf, snd-it wf, decidable wf, es-loc wf, bool wf, es-dtype wf, Id wf, fifoC wf, es-E wf, fifoR wf, rcv-it wf, not wf, es-causle wf, es-causl wf, fifoS wf